Die Computation Tree Logic (kurz CTL) ist eine Temporale Logik, die speziell zur Spezifikation und Verifikation von Computersystemen dient. Eine bestimmte Verallgemeinerung der unten beschriebenen Logik, für die der Name CTL steht, wird als CTL* bezeichnet. CTL bezeichnet dann eine spezielle Teilmenge der CTL*-Formeln. Eine weitere wichtige spezi...